Majumdar R., “Software model checking

Software model checking is the algorithmic analysis of programs to prove prop-erties of their executions. It traces its roots to logic and theorem proving, both to provide the conceptual framework in which to formalize the fundamental questions and to provide algorithmic procedures for the analysis of logical questions. The undecidability theorem [Turing 1936] ruled out the possibility of a sound and com-plete algorithmic solution for any sufficiently powerful programming model, and even under restrictions (such as finite state spaces), the correctness problem re-mained computationally intractable. However, just because a problem is hard does not mean it never appears in practice. Also, just because the general problem is undecidable does not imply that specific instances of the problem will also be hard. As the complexity of software systems grew, so did the need for some reasoning mechanism about correct behavior. (While we focus here on analyzing the behav-ior of a program relative to given correctness specifications, the development of specification mechanisms happened in parallel, and merits a different survey.) Initially, the focus of program verification research was on manual reasoning, an